A:Type, B:(AType), f:a:A fp B(a), eq:EqDecider(A).   f = f 

latex

Definitions	car.cdr, ||as||, s = t, type List, f(a), reduce(f;k;as), Case b of inl(x)  s(x) ; inr(y)  t(y), if b t else f fi, Case of a; nil  s ; x.y, rec:z  t(x;y;z), Y, x:A. B(x), t  T, x:AB(x), (x  l), {x:A| B(x) }, <a,b>, x(s), f(x), x  dom(f), f(x)?z, f  g, , a:A fp B(a), x:AB(x), Type, x. t(x), EqDecider(T), P & Q, true, x.A(x), filter(P;l), s ~ t
Lemmas	deq wf, fpf wf, l member wf